Nuprl Definition : atom2-deq
11,40
postcript
pdf
atom2-deq == <
a
,
b
. eq_atom{2:n}(
a
;
b
), TERMOF{
atom2-deq-aux
:ObjectId, 1:l}>
latex
Definitions
<
a
,
b
>
,
x
.
A
(
x
)
,
eq_atom{$n:n}(
x
;
y
)
,
atom2-deq-aux
FDL editor aliases
atom2-deq
origin
a,b. eq_atom{2:n}(a; b), TERMOF{atom2-deq-aux:ObjectId, 1:l}> a,b. eq_atom{2:n}(a; b), TERMOF{atom2-deq-aux:ObjectId, 1:l}> x.A(x)